\subsection{???}
Given a linear order \( \eta \), we will write \( [\eta]^k \) for the set of ordered \( k \)-tuples in \( \eta \):
\[ [\eta]^k = \qty{\vb a \in \eta^k \midd a_0 <^\eta a_1 <^\eta \dots <^\eta a_{k-1}} \]
\begin{definition}
	Let \( \mathcal M \) be an \( \mathcal L \)-structure, let \( \Phi \) be a set of \( \mathcal L \)-formulae, and let \( \eta \) be a strict chain of elements of \( \mathcal M \).
	We say that \( \eta \) is \emph{\( \Phi \)-indiscernible} in \( \mathcal M \) if
	\[ \mathcal M \vDash \phi(\vb a) \Leftrightarrow \phi(\vb b) \]
	for all \( \vb a, \vb b \in [\eta]^k \) of the correct length and \( \varphi \in \Phi \).
	We simply say that \( \eta \) is a sequence of indiscernibles if the above holds where \( \Phi \) is the set of every \( \mathcal L \)-formula.
\end{definition}
\begin{example}
	\begin{enumerate}
		\item Any linearly ordered basis \( \mathcal B \) for a vector space provides a sequence of indiscernibles.
			Indeed, given \( \vb a, \vb b \in [\mathcal B]^k \), there is an automorphism of the vector space that maps \( \vb a \) to \( \vb b \).
		\item Any chain of algebraically independent elements in a field \( k \vDash \mathsf{ACF}_0 \) is a sequence of indiscernibles.
		\item If \( R \) is a ring, then the variables \( X_1, \dots, X_n \) form a set of indiscernibles of \( R[X_1, \dots, X_n] \).
	\end{enumerate}
\end{example}
\begin{definition}
	An \emph{Ehrenfeucht--Mostowski functor} is a mapping \( F \) that takes each linear order \( \eta \) to an \( \mathcal L \)-structure \( F(\eta) \), and each order embedding \( g : \eta \rightarrowtail \varepsilon \) to an embedding of \( \mathcal L \)-structures \( F(g) : F(\eta) \rightarrowtail F(\varepsilon) \), in such a way that
	\begin{enumerate}
		\item each \( \eta \) generates \( F(\eta) \), that is, \( \eta \subseteq F(\eta) \) as sets, and every element of \( F(\eta) \) is of the form \( t^{F(\eta)}(\vb a) \) where \( t(\vb x) \) is an \( \mathcal L \)-term and \( \vb a \in [\eta]^k \);
		\item for each order embedding \( g : \eta \rightarrowtail \varepsilon \), the embedding of \( \mathcal L \)-structures \( F(g) \) extends \( g \);
		\item for every linear order \( \eta \), we have \( F(1_\eta) = 1_{F(\eta)} \);
		\item for each composable pair of embeddings \( f, g \), we have \( F(g\circ f) = F(g)F(f) \).
	\end{enumerate}
\end{definition}
In particular, every automorphism of a linear order \( \eta \) induces an automorphism of \( F(\eta) \).
\begin{proposition}[sliding property]
	Let \( F \) be an Ehrenfeucht--Mostowski functor, let \( \eta, \varepsilon \) be linear orders, and let \( \vb a \in [\eta]^k, \vb b \in [\varepsilon]^k \).
	Then for every quantifier-free formula \( \varphi(x_1, \dots, x_k) \), we have
	\[ F(\eta) \vDash \varphi(\vb a) \iff F(\varepsilon) \vDash \varphi(\vb b) \]
\end{proposition}
\begin{proof}
	Embed \( \eta \) and \( \varepsilon \) into some linear order \( \rho \) in which \( \vb a \) and \( \vb b \) are identified.
	Let \( f : \eta \to \rho \) and \( g : \varepsilon \to \rho \) be the embeddings.
	Suppose that \( F(\eta) \vDash \varphi(\vb a) \).
	As embeddings preserve quantifier-free formulae and the map \( F(f) : F(\eta) \rightarrowtail F(\rho) \) extends \( f \), we must have that \( F(\rho) \vDash \varphi(f(\vb a)) \).
	As \( f(\vb a) = g(\vb b) \), we must have \( F(\rho) \vDash \varphi(g(\vb b)) \), and so for the same reason, \( F(\varepsilon) \vDash \varphi(\vb b) \).
\end{proof}
We see that the chain \( \eta \subseteq F(\eta) \) is indiscernible by quantifier-free formulas.
\begin{definition}
	Let \( \mathcal M \) be an \( \mathcal L \)-structure containing a linear order \( \eta \subseteq \mathcal M \) as sets.
	Then, we define the theory of \( \eta \) in \( \mathcal M \), denoted \( \operatorname{Th}(\mathcal M, \eta) \), to be the set of all \( \mathcal L \)-formulae \( \varphi(\vb x) \) that are satisfiable in \( \mathcal M \) by every ordered tuple \( \vb a = a_0 < \dots < a_{k-1} \) in \( \eta \).
	The theory \( \operatorname{Th}(F) \) of an Ehrenfeucht--Mostowski functor \( F \) is the set of all \( \mathcal L \)-formulae \( \varphi(\vb x) \) such that \( F(\eta) \vDash \varphi(\vb a) \) for every linear order \( \eta \) and ordered tuple \( \vb a \) in \( \eta \).
\end{definition}
\begin{lemma}
	Let \( \eta \) be an infinite linear order, let \( F \) be an Ehrenfeucht--Mostowski functor, and let \( \varphi \) be a universal sentence that is true in \( F(\eta) \).
	Then \( \varphi \in \operatorname{Th}(F) \).
\end{lemma}
\begin{proof}
	Let \( \varphi = \forall \vb x.\, \psi(\vb x) \) where \( \psi \) is quantifier-free.
	Let \( \varepsilon \) be a linear order, and let \( \vb a \in F(\varepsilon) \); we need to show \( F(\varepsilon) \vDash \psi(\vb a) \).
	As \( \varepsilon \) generates \( F(\varepsilon) \), there is a finite suborder \( \varepsilon_0 \) such that \( \vb a \in F(\varepsilon_0) \).
	But \( \eta \) is infinite, so there is an embedding \( f : \varepsilon_0 \rightarrowtail \eta \).
	By assumption, \( F(f)(\vb a) \) satisfies \( \psi \) in \( F(\eta) \), so \( F(\varepsilon_0) \vDash \psi(\vb a) \), as \( \psi \) is quantifier-free so is preserved under substructures.
	Similarly, \( F(\varepsilon) \vdash \psi(\vb a) \), as required.
\end{proof}
\begin{lemma}[stretching property]
	Let \( \mathcal M \) be an \( \mathcal L \)-structure that contains the linear order \( \omega \) as a generating set.
	Suppose that \( \omega \) is indiscernible by quantifier-free formulae.
	Then there is an Ehrenfeucht--Mostowski functor \( F \) such that \( \mathcal M = F(\omega) \).
	Moreover, if \( G \) is another such functor, then there is an isomorphism \( \alpha : F(\eta) \to G(\eta) \) for each linear order \( \eta \), and \( \eval{\alpha}_\eta = 1_\eta \).
\end{lemma}
\( F \) is unique up to natural isomorphism.
% TODO: Proof on ES3.
\begin{definition}
	Let \( F \) be an Ehrenfeucht--Mostowski functor, and let \( \mathcal T \) be a theory.
	The models of \( \mathcal T \) that are of the form \( F(\eta) \) are called \emph{Ehrenfeucht--Mostowski models} of \( \mathcal T \).
\end{definition}
\begin{theorem}[Ramsey]
	Let \( X \) be a countable linear order, and let \( k, n \) be positive integers.
	Then for every function \( f : [X]^k \to n \), there is an infinite subset \( Y \subseteq X \) such that \( f \) is constant on \( [Y]^k \).
\end{theorem}
We will use Ramsey's theorem to show that Ehrenfeucht--Mostowski models for Skolem theories with infinite models always exist.
\begin{lemma}
	Let \( F \) be an Ehrenfeucht--Mostowski functor such that \( \operatorname{Th}(F(\omega)) \) is Skolem.
	Then \( \operatorname{Th}(F) \) includes either \( \varphi(\vb x) \) or \( \neg\varphi(\vb x) \) for every \( \mathcal L \)-formula \( \varphi(\vb x) \).
	In particular, all of the \( F(\eta) \) are elementarily equivalent, and each linear order \( \eta \) is indiscernible in \( F(\omega) \).
\end{lemma}
\begin{proof}
	Since \( \operatorname{Th}(F(\omega)) \) is Skolem, it admits a universal axiomatisation.
	Moreover, every formula is equivalent to a quantifier-free formula modulo \( \operatorname{Th}(F(\omega)) \).
	The result then follows from the sliding property and the lemma on universal sentences.
\end{proof}
\begin{theorem}[Ehrenfeucht--Mostowski theorem]
	Let \( \mathcal M \) be an \( \mathcal L \)-structure, and suppose that \( \operatorname{Th}(\mathcal M) \) is Skolem.
	If \( \eta \) is infinite linear order that is contained as a set in \( \mathcal M \), then there is an Ehrenfeucht--Mostowski functor \( F \) in \( \mathcal L \) whose theory expands \( \operatorname{Th}(\mathcal M,\eta) \).
\end{theorem}
\begin{proof}
	We want to build a theory extending \( \operatorname{Th}(\mathcal M, \eta) \), whose models include an indiscernible copy of \( \omega \).
	First, expand \( \mathcal L \) to add \( \omega \)-many constants \( C = \qty{c_i \mid i \in \omega} \), and we build an \( \mathcal L_C \)-theory \( \mathcal T \) with the following axioms:
	\begin{enumerate}
		\item \( \varphi(\vb a) \Leftrightarrow \varphi(\vb b) \), for each \( \mathcal L \)-formula \( \varphi(\vb x) \) and ordered tuples \( \vb a, \vb b \in [C]^{\abs{\vb x}} \);
		\item \( \varphi(c_0, \dots, c_{k-1}) \), for each formula \( \varphi(x_0, \dots, x_{k-1}) \) in \( \operatorname{Th}(\mathcal M, \eta) \).
	\end{enumerate}
	We will show that this theory has a model by compactness.
	Let \( \mathcal U \) be a finite subset of \( \mathcal T \), and list the formulae in \( \mathcal U \) as \( \varphi_0, \dots, \varphi_{m-1} \).
	Note that there is some finite \( k \) such that the new constants that show up in the formulae in \( \mathcal U \) are among \( c_0, \dots, c_{k-1} \).
	By adding redundant variables, we may assume that each of these formulae all have free variables \( c_0, \dots, c_{k-1} \) for simplicity.

	Define an equivalence relation \( \sim \) on \( [\eta]^k \) by declaring that \( \vb a \sim \vb b \) if \( \mathcal M \vDash \varphi_j(\vb a) \) if and only if \( \mathcal M \vDash \varphi_j(\vb b) \) for each \( j < m \).
	This equivalence relation partitions \( [\eta]^k \) into finitely many equivalence classes.
	Hence, by Ramsey's theorem, there is an infinite sequence \( \vb e = e_0 < e_1 < \dots < e_{2k-1} \) in \( \eta \) such that any two ordered \( k \)-tuples extracted from \( \vb e \) are in the same equivalence class.
	We can interpret each \( c_j \) in \( \mathcal M \) as \( e_j \) for each \( j < k \), making \( \mathcal M \) into an \( \mathcal L_{\vb c} \)-structure that models \( \mathcal U \).

	Let \( \mathcal N \) be a model of \( \mathcal T \).
	The new constants \( c_i \) must be interpreted as different elements of \( \mathcal N \), as \( \operatorname{Th}(\mathcal M, \eta) \) includes the sentence \( x_0 \neq x_1 \).
	Hence \( \mathcal N \) contains a copy of \( \omega \), by seeing \( c_i \) in \( \mathcal N \) as \( i \).
	Consider \( \mathcal N^\star \), which is the \( \mathcal L \)-reduct of \( \mathcal N \), and let \( \mathcal S = \langle \omega \rangle_{\mathcal N^\star} \).
	Note that \( \operatorname{Th}(\mathcal M, \eta) \) is contained in \( \operatorname{Th}(\mathcal N^\star, \omega) \).
	This in particular implies that \( \operatorname{Th}_{\mathcal L}(\mathcal N^\star) \) is Skolem, as \( \operatorname{Th}(\mathcal M) \) is Skolem and \( \operatorname{Th}(\mathcal M) \subseteq \operatorname{Th}(\mathcal M, \eta) \).
	It then follows that \( \mathcal S \) is an elementary substructure of \( \mathcal N^\star \), and is generated by \( \omega \).
	Then, \( \operatorname{Th}(\mathcal M, \eta) \subseteq \operatorname{Th}(\mathcal S, \omega) \).
	Finally, sentences in \( \mathcal T \) ensure that \( \omega \) is indiscernible in \( \mathcal S \) by construction, so the stretching lemma gives an Ehrenfeucht--Mostowski functor \( F \) with \( \mathcal S = F(\omega) \), which completes the proof by the previous lemma.
\end{proof}
